perm filename XXX[1,JRA]2 blob sn#016819 filedate 1972-12-12 generic text, type T, neo UTF8
00100	PRE_OP:A,B,U,f,SB;
00200	INF_OP:∩;
00300	INF_PRED:ε,≡,⊂;
00400	VAR: x,y,z,u,v,X,Y,Z,V;
00500	A1:f((SB(A)∩SB(B)),SB((A∩B)))ε(SB(A)∩SB(B));
00600	A2:¬f((SB(A)∩SB(B)),SB((A∩B)))εSB(x);
00700	;
00900	a5:(z⊂x ∧ z⊂y)↔ z⊂x∩y;
01000	a7:(z⊂x∧zεU) ↔zεSB(x);
01100	THEOREM: SB(A)∩SB(B) ≡ SB(A∩B);
01200	;
01300	e